$\forall$$T$:Type, ${\it as}$:$T$ List. ($\lambda$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it as}$$\parallel$}}$. ${\it as}$[$i$])\{$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it as}$$\parallel$}}$\} $=$ ${\it as}$